T:Type, L1, L2, L:T List.
interleaving(T;L1;L2;L)
 (f1:(||L1||||L||), f2:(||L2||||L||). interleaving_occurence(T;L1;L2;L;f1;f2)) 

latex

Definitions	t  T, True, P & Q, x:A. B(x), ij, ||as||, {i..j}, P  Q, False, A, AB, T, , Prop, l[i], S  T, S  T, increasing(f;k), x:A. B(x), disjoint_sublists(T;L1;L2;L), interleaving_occurence(T;L1;L2;L;f1;f2), interleaving(T;L1;L2;L)
Lemmas	interleaving wf, nat wf, increasing wf, int seg wf, select wf, not wf, length wf1, non neg length